\begin{tabbing}
R{-}Feasible(\=ecl{-}machine at "b" with state ecl\+
\\[0ex]
\\[0ex]eclcatch([eclseq(ecland(eclbase(rcv(lnk1\{input to b\},"play");$\lambda$$s$,$v$.
\\[0ex]true$_{2}$);eclbase(locl("choose1");$\lambda$$s$,$v$.
\\[0ex]true$_{2}$));eclor(eclthrow(eclbase(locl("diff");$\lambda$$s$,$v$.
\\[0ex]true$_{2}$);1);eclbase(locl("same");$\lambda$$s$,$v$. true$_{2}$)))]$\ast$;[1]).1
\\[0ex]
\\[0ex]state variables "x1" : $\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$ $\oplus$ "v1" : $\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$ $\oplus$ "win" : $\mathbb{Z}$ $\oplus$ "x2" : $\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$ $\oplus$ "v2" : $\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$
\\[0ex]
\\[0ex]actions \=rcv(lnk1\{input to b\},"play") : $\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$ $\oplus$ locl("choose1") : Unit $\oplus$ \+
\\[0ex]locl("diff") : Unit $\oplus$ 
\\[0ex]locl("same") : Unit $\oplus$ rcv(lnk1\{b to output\},"hello") : $\mathbb{B}$
\\[0ex]
\-\\[0ex]sends l\=ocl("diff") sends on lnk1\{b to output\}\+
\\[0ex]with tag "hello" [$s$,$v$.rps($s$("x1");$s$("v1"))], at marker 1
\\[0ex]
\-\\[0ex]updates update{-}spec1(locl("diff");"win";1;$s$,$v$.$s$("win")+\=if \=rps($s$("x1");$s$("v1"))$\rightarrow$\+\+
\\[0ex]1
\-\\[0ex]else 0 fi)
\-\-\\[0ex]$\oplus$ \=(@"b" \=precondition for "diff"(v:Unit):\+\+
\\[0ex]$\lambda$$s$,$v$. $\neg$$s$("x1") $=$ $s$("v1") $\in$ $\mathbb{Z}$ State("x1" : $\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$ $\oplus$ "v1" : $\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$) v
\-\\[0ex]$\oplus$ @"b" \=precondition for "same"(v:Unit):\+
\\[0ex]$\lambda$$s$,$v$. $s$("x1") $=$ $s$("v1") $\in$ $\mathbb{Z}$ State("x1" : $\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$ $\oplus$ "v1" : $\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$) v)
\-\-\\[0ex]$\oplus$ @"b" \=precondition for "choose1"(v:Unit):\+
\\[0ex]$\lambda$$s$,$v$. True State() v
\-\\[0ex]$\oplus$ @"b" effect rcv(lnk1\{input to b\},"play")(v:$\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$)  "x1" := $\lambda$$s$,$v$. $v$ State("x1" : $\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$) v 
\\[0ex]$\oplus$ @"b" effect locl("choose1")(v:Unit)  "v1" := $\lambda$$s$,$v$. random(0;2) State("v1" : $\mathbb{N}$$_{\mbox{\scriptsize $<$3}}$) v )
\end{tabbing}